package utils

import chisel3._
import chisel3.util._
import chisel3.util.experimental._
import chiseltest._

import chiseltest.formal._
import chiseltest.experimental._
import chisel3.stage.{ChiselStage, ChiselGeneratorAnnotation}

import org.scalatest.Tag
import org.scalatest.flatspec.AnyFlatSpec

import chiseltest.ChiselScalatestTester
import chiseltest.formal.backends.FormalEngineAnnotation

class FormalLockingArbiterSpec extends AnyFlatSpec with ChiselScalatestTester with Formal {

  // "LockingAribter" should "pass" in {
  //   verify(new LockingAribterSpec, Seq(BoundedCheck(50), BtormcEngineAnnotation))
  // }

//   "Simulation based test" should "pass" in {

//     val FAN_IN = 4
//     val LOCK_CYCLES = 8

//     test (new LockingArbiter(Flipped(Vec(FAN_IN, Decoupled(UInt(2.W)))), FAN_IN, LOCK_CYCLES)) { arb => 

//       arb.io.out.ready.poke(true.B)
//       for (i <- 0 to FAN_IN - 1) {
//         arb.io.in(i).valid.poke(false.B)
//       }
//       arb.io.in(FAN_IN - 1).valid.poke(true.B)
//       for (k <- 0 to LOCK_CYCLES * 2 - 1) {
//         arb.clock.step()
//         println("CHOSEN: " + arb.io.chosen.peek().litValue + " VALID: "+ arb.io.out.valid.peek().litValue)

//         if (k == 3) {
//           arb.io.in(FAN_IN - 1).valid.poke(false.B)
//         }


//         if (k == 5) {
//           arb.io.in(FAN_IN - 1).valid.poke(true.B)
//         }


//         if (k < FAN_IN - 1) {
//           arb.io.in(k).valid.poke(true.B)
//         }

//       }
//       arb.io.in(FAN_IN - 1).valid.poke(false.B)


//     }


//   }

}

// class LockingAribterSpec extends Module {
//  
//   val FAN_IN = 4
//   val LOCK_CYCLES = 8

//   val io = IO(new Bundle {
//     val in = Flipped(Vec(FAN_IN, Decoupled(UInt(2.W))))
//     val out = Decoupled(UInt(2.W))
//   })

//   val lockArb = Module(new LockingArbiter(chiselTypeOf(io.in(0).bits), FAN_IN, LOCK_CYCLES))

//   lockArb.io.in <> io.in

//   io.out <> lockArb.io.out

//   assume(io.out.ready)

//   assert(!(io.))
// }
